WrongSizeAssignment.agda:17,1-18,23
Termination checking failed for the following functions:
  f
Problematic calls:
  f {i} (suc {i ^} (lift {i ^} x))
    (at WrongSizeAssignment.agda:18,7-8)
